$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $B$:($A$$\rightarrow$Type), $P$:($A$$\rightarrow\mathbb{B}$), $f$:$x$:$A$ fp$\rightarrow$ $B$($x$), $x$:$A$, $v$:$B$($x$).
\\[0ex]($\langle$$x$$,\,$$v$$\rangle$ $\in$ fpf{-}vals(${\it eq}$;$P$;$f$)) $\Leftrightarrow$ \{$x$ $\in$ dom($f$) \& $P$($x$) \& $v$ $=$ $f$($x$)\}